/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */
package alloy.semantic;

import java.util.Collections;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.Assertion;
import alloy.ast.Decl;
import alloy.ast.Fact;
import alloy.ast.FormulaPara;
import alloy.ast.Function;
import alloy.ast.Id;
import alloy.ast.Ids;
import alloy.ast.Module;
import alloy.ast.Modules;
import alloy.ast.Path;
import alloy.ast.Predicate;
import alloy.ast.Signature;
import alloy.ast.Variable;
import alloy.util.Dbg;

/**
 * A visitor which gathers all the ids in a given module.  The ids
 * are used to determine which paragraphs, when being imported from 
 * a module, must be fully qualified and which do not have to be.
 * 
 * @see 
 */
public class IdGatheringVisitor extends ASTDepthFirstVisitor {

	private Set _identifiers;
	
	public IdGatheringVisitor() {
		_identifiers = new HashSet();
	}
	
	public Set getIds() {
		return Collections.unmodifiableSet(_identifiers);
	}

	public void visit(Modules modules_) {
		Dbg.fatal("should not be called on modules");
	}
	
    /**
     * Visits the constructs of the module.
     */
    public void visit(Module module_) {
        // visit signatures, facts, functions, and assertions
        module_.getSignatures().applyVisitor(this);
        module_.getFunctions().applyVisitor(this);
        module_.getPredicates().applyVisitor(this);
        module_.getFacts().applyVisitor(this);
        module_.getAssertions().applyVisitor(this);
    }

    /**
     * check all the type parameters and fields of the
     * signature, plus any quantified variables appearing in the
     * fact
     */
    public void visit(Signature signature_) {
        // check the field declarations
        signature_.getDecls().applyVisitor(this);
        // check the fact if it is non-empty
        Fact fact = signature_.getFact();
        if (!fact.isEmpty()) {
            fact.applyVisitor(this);
        }
    }

    /**
     * check all the type parameters and any quantified variables appearing
     * in the formulas
     */
    public void visit(FormulaPara formulaPara_) {
        // check quantified variables in formulas
        formulaPara_.getFormula().applyVisitor(this);
    }

    public void visit(Fact fact_) {
        visit((FormulaPara)fact_);
    }

    public void visit(Assertion assertion_) {
        visit((FormulaPara)assertion_);
    }

    public void visit(Function function_) {
        // have to avoid "functionName =" portion of formula
        function_.getExpression().applyVisitor(this);
        function_.getArgList().getDecls().applyVisitor(this);
    }

    public void visit(Predicate predicate_) {
        visit((FormulaPara)predicate_);
        predicate_.getArgList().getDecls().applyVisitor(this);
    }

    public void visit(Path path_) {
	// we don't want to check inside paths
	return;
    }

    /**
     * check if the variables of the declaration shadow
     */
    public void visit(Decl decl_) {
        // just visit the variables, should hit all the Ids
        decl_.getVariables().applyVisitor(this);
    }

    /**
     * add each identifier
     */
    public void visit(Ids ids_) {
        Iterator idIter = ids_.getIdIter();
        while (idIter.hasNext()) {
            add((Id)idIter.next());
        }
    }

    /**
     * adds the identifier
     */
    public void visit(Variable variable_) {
        add(variable_.getId());
    }
    
    public void add(Id id_) {
    	_identifiers.add(id_.nodeString());
    }

}

